x,y:. (x z y)  (x  y) 

latex

ProofTree

Definitions	t  T, A  B, i z j, x:A. B(x), P  Q, P  Q, P  Q, P  Q,
Lemmas	assert of bnot, iff functionality wrt iff, not wf, lt int wf, bnot wf, assert wf, assert of lt int, not functionality wrt iff